Notes on knowledge

Let's formalize knowledge using circumscription.

Key axiom:

cancels(x,y) ∧ applies(x,s) ⊃ ab aspect1(y,s).

This is intended to allow cancellation of inheritance, but
it isn't quite right.

We want a general axiom that says that people know the effects
of their possible actions.  It should be cancellable by consideration
that says they don't, e.g. a person doesn't ordinarily know the
combination of a safe, but he ordinarily does if it's his safe.

relevant(x,p,s) ∧ ¬ab aspect1(p,x,s) ⊃ holds(knows(p,x),s)

cancels(issafe y,knows(p,combination y))